da:k:Knd fp Type, k:Knd. Normal(da)  Normal(Valtype(da;k)) 

latex

Definitions	Normal(da), Valtype(da;k), xdom(f). v=f(x)   P(x;v), f(x)?z, if b t else f fi, f(x), left+right, Unit, P  Q, P & Q, x:AB(x), x  dom(f), KindDeq, x:AB(x), a:A fp B(a), x. t(x), x.A(x), Type, Knd, Prop, s = t, , b, A, b, P  Q, t  T, x:A. B(x), Normal(T), Top
Lemmas	normal-top, assert wf, not wf, bnot wf, bool wf, Knd wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, fpf-ap wf, normal-type wf